perm filename AXIOM.LSP[1,JRA] blob
sn#015596 filedate 1972-12-04 generic text, type T, neo UTF8
(DEFPROP FOO
(NIL FOO
APPENDIT
ATTEMPT
ATTEMPTUNTIL
ATTEMPT1
AUTO
CHOICE1
GOLIST
INCLAUSES
INITIAL
INITIALAX
INITIALAX1
NEGATE
PRECNF
PROOF1
PROOF
QUERY
RESET1
SAVE1
SET1
SETQUERY1
SETQUERY2
SETUP
TREE
TREEDEP
TRY1
TRAVERSE
UPDATE
UPGETL)
VALUE)
(DEFPROP APPENDIT
(LAMBDA(X Y)
(PROG NIL (COND (USINGFL (SETQ USING (CONS N2 (APPEND (REVERSE Y) USING))))) (RETURN (APPEND X Y))))
EXPR)
(DEFPROP ATTEMPT
(LAMBDA(Z S C)
(PROG (NEWNAME SUPPORT
EDITSTRAT
LCL
LVL
CNT
XYZ2
LSTCLS
LLST
Z1
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
STRATEGY
STRAT
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST
XYZ
XYZ1
COND
UNAXP
UNAXN
SAT
EE
EE1
XX
CLAUSES
SUBCLAUSES
COUNT)
(SETQ TBL (SET1 (APPEND PREFN INFN)))
(SET3 Z)
(SETQ Z (MINIMIZE Z))
(SETQ NEWNAME (INITIAL Z))
(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
(SETQ COND C)
(SETQ XYZ2 Z)
(SETQ LVL 1)
(SETQ COUNT 0)
(SETQ Z (UNITPN XYZ2))
(SETQ UNAXP (CAR Z))
(SETQ UNAXN (CDR Z))
(SETQ CLAUSES XYZ2)
(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
(SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
(T (SETQ SUBCLAUSES CLAUSES)))
(SETQ LCL (LAST CLAUSES))
(SETQ LSTCLS LCL)
(COND (ANCESTRY (GO AA)))
(SETQ XX (CONS CLAUSES CLAUSES))
(SETQ EE CLAUSES)
(SETQ EE1 (LAST EE))
(SETQ CNT (LENGTH XYZ2))
BB (SETQ Z1 (ERRSET (ATTEMPT1 XYZ2)))
(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (SETQUERY1 CLAUSES STRAT)))
((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
(EVAL
(LIST (QUOTE OUTC)
(LIST (QUOTE OUTPUT)
(QUOTE PRF)
(QUOTE DSK:)
(CONS (READLIST
(CONS (QUOTE #)
(CONS (SETQ PRNO (ADD1 PRNO))
FILENAM)))
(QUOTE PRF)))
NIL)))
(QUERY)
(PROOF LHP RHP)
(OUTC Z T)
(RETURN Z1))
(T (RETURN Z1)))
AA (SETQ XYZ XYZ2)
(SETQ EE CLAUSES)
(SETQ EE1 (LAST CLAUSES))
CC (SETQ LLST (CONS (CAR XYZ) LLST))
(SETQ XYZ (CDR XYZ))
(COND (XYZ (GO CC)) (T (GO BB)))))
EXPR)
(DEFPROP ATTEMPTUNTIL
(LAMBDA (L S C) (ATTEMPT (INITIALAX L) S C))
EXPR)
(DEFPROP ATTEMPT1
(LAMBDA (L) (COND (ANCESTRY (ANCESTRY LLST)) (T (TRYPRF L))))
EXPR)
(DEFPROP AUTO
(LAMBDA(XX)
(PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
(COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
(SETQ PDEPTH 3)
(SETQ DDEPTH 4)
(COND
((NULL EQUAL) (PRINT (QUOTE (IS THERE AN EQUALITY PREDICATE (Y / N))))
(COND
((EQ (READ) (QUOTE Y)) (PRINT (QUOTE (WHAT IS IT)))
(SETQ PFLG NIL)
(SETQ EQUAL (READ))))))
(SETQ X1 XX)
(SETQ M (SETQ D 0))
A (SETQ M (MAX M (LENGTH (CDAR X1))))
(SETQ D (MAX D (DEPTH (CDAR X1))))
(SETQ Z2 (CAR X1))
(COND
((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
(SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
(SETQ X1 (CDR X1))
(COND ((CDR X1) (GO A)))
(SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
(COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
B (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
C (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
(COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
(COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
(COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
(COND (SUPPORT (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))))
(SETQ ANCESTRY T)
(SETQ EDITSTRAT
(QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
(SETQ DEBUG T)
(COND (DLIST (SET3 DLIST)))
(RETURN
(LIST STRATEGY
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST))))
EXPR)
(DEFPROP AUTO
(NIL . T)
VALUE)
(DEFPROP CHOICE1
(LAMBDA (L LL) (COND ((ATOM (CDR (ANCESTOR L))) LL) (T (NCONC (CDR (TRAVERSE L)) LL))))
EXPR)
(DEFPROP GOLIST
(NIL (EO . UEO1)
(DS . UDS1)
(CH . UCH1)
(SY . USY1)
(CU . UCU1)
(FL . UFL1)
(DI . UDI1)
(ST . UST1)
(HA . UST1)
(DE . UDE1)
(IN . UIN1)
(EV . UEV1)
(QU . UQU1)
(TR . UTR1)
(UP . UUP1)
(ME . UME1)
(SI . USI1)
(SE . USE1)
(DO . UDO1)
(CL . UCL1)
(SU . USU1)
(AN . UAN1)
(TE . UTE1)
(RE . URE1)
(SA . USA1)
(PA . UPA1)
(AS . UAS1)
(ED . UED1)
(US . UUS1)
(PR . UPR1)
(FU . UFL2)
(FD . UFL3)
(GO . UGO1)
(EX . UEX1)
(AB . UAB1)
(HE . UHE1))
VALUE)
(DEFPROP INCLAUSES
(LAMBDA NIL
(PROG (Z AXNO)
(SETQ AXNO (QUOTE AXIOM))
A (SCANSET)
(START)
(SETQ ZIN (ERRSET (<INPUT>) T))
(SCANRESET)
(COND ((OR (NULL ZIN) (NULL (CAR ZIN))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ ZIN (TOP))
(COND ((EQ ZIN (QUOTE EMPTY)) (RETURN Z)) ((ATOM ZIN) (PRIN1 ZIN) (SETQ AXNO (SETQ FNNAM ZIN)) (GO A)))
(OUT >S< ZIN)
(SETQ Z
(APPEND Z
(SETUP
(CNF
(COND ((EQ AXNO (QUOTE THEOREM)) (LIST (QUOTE NOT) (FIXQFF ZIN))) (T (FIXQFF ZIN)))))))
(GO A)))
EXPR)
(DEFPROP INITIAL
(LAMBDA(L)
(PROG (ST Z Z1 Z2)
A (SETQ Z (CDR (ANCESTOR (CAR L))))
(COND ((NOT (ATOM Z)) (PRINT (QUOTE LOSE-IN-INITIAL)) (ERR NIL))
((SETQ Z1 (ASSOC Z ST)) (RPLACD (LAST Z1) (LIST (CAR L))))
(T (SETQ ST (CONS (CONS Z (LIST (CAR L))) ST))))
(SETQ Z2 (CONS (CAR L) Z2))
(SETQ L (CDR L))
(COND (L (GO A)))
(RETURN (REVERSE (CONS (CONS NIL NIL) (CONS (CONS (QUOTE %INITIAL) (REVERSE Z2)) ST))))))
EXPR)
(DEFPROP INITIALAX
(LAMBDA(L)
(PROG (Z Z1 Z2 Z3 AXNO)
(SETQ AXNO (CAR L))
(SETQ L (CDR L))
A (SETQ Z (CAR (SETUP (LIST (COPY (CDAR L))))))
(SETQ Z1 (ANCESTOR (CAR L)))
(COND ((ATOM (CAR Z1)) (SETQ Z1 (CDR Z1))))
(SETQ Z2 (ANCESTOR Z))
(RPLACA Z2 Z1)
(RPLACD Z2 AXNO)
(SETQ Z3 (CONS Z Z3))
B (SETQ L (CDR L))
(COND ((NULL L) (RETURN (REVERSE Z3))) ((ATOM (CAR L)) (SETQ AXNO (CAR L)) (GO B)))
(GO A)))
EXPR)
(DEFPROP INITIALAX1
(LAMBDA(L1)
(PROG (Z L2 L)
(SETQ L L1)
B1 (SETQ L2 L)
A1 (COND ((EQ (CAR L) (CADR L2)) (RPLACD L2 (CDDR L2)) (GO A1)))
(SETQ L2 (CDR L2))
(COND (L2 (GO A1)))
(SETQ L (CDR L))
(COND (L (GO B1)))
(SETQ L L1)
B (SETQ Z (CDDAAR L))
(COND ((NULL (CAAAR L)) (RPLACA (CAAR L) (LENGTH (CDAR L))))
((NUMBERP (CAAAR L)) NIL)
(T (RPLACA (CAAR L) (CAAAAR L))))
(COND ((ATOM (CDDR Z)) (GO A)))
(RPLACD Z (CONS (CDR Z) (QUOTE DEDUCT)))
A (SETQ L (CDR L))
(COND (L (GO B)))
(RETURN L1)))
EXPR)
(DEFPROP NEGATE
(LAMBDA(Z)
(PROG (BDY)
A (SETQ Z (CDR Z))
(COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
(SETQ Z (CDDR Z))
C (COND ((NULL Z) (GO D)))
(SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
(SETQ Z (CDR Z))
(GO C)
D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
EXPR)
(DEFPROP PRECNF
(LAMBDA(X)
(COND ((EQ (CAR X) (QUOTE NOT)) (LIST (QUOTE NOT) (PRECNF (CADR X))))
((MEMQ (CAR X) (QUOTE (AND OR))) (LIST (CAR X) (PRECNF (CADR X)) (PRECNF (CADDR X))))
((MEMQ (CAR X) (QUOTE (FA TE))) (LIST (CAR X) (CADR X) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE IMP)) (LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X))))
((EQ (CAR X) (QUOTE EQUIV))
(LIST (QUOTE AND)
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (CADR X))) (PRECNF (CADDR X)))
(LIST (QUOTE OR) (LIST (QUOTE NOT) (PRECNF (COPY (CADDR X)))) (PRECNF (COPY (CADR X))))))
(T X)))
EXPR)
(DEFPROP PROOF1
(LAMBDA(L)
(PROG (Q X Y Z P P1)
(PRINC (QUOTE / ))
(PRINC (QUOTE / ))
(PRFPRINT (CDR L))
(SETQ P (ANCESTOR L))
(COND ((ATOM (CDR P)) (GO P3)))
(SETQ P1 (CDR P))
(SETQ P (CAR P))
(PRINC (QUOTE / ))
(PRINC 1)
(PRINC (QUOTE / ))
(PRINC 2)
(SETQ X 1)
(SETQ Y 2)
(SETQ Q (LIST (CONS X P) (CONS Y P1)))
P1 (SETQ Z (ANCESTOR (CDAR Q)))
(COND ((ATOM (CDR Z)) (PRINT (CAAR Q)) (PRFPRINT (CDDAR Q)) (PRIN1 (CDR Z)) (GO P2)))
(SETQ X (ADD1 Y))
(SETQ Y (ADD1 X))
(PRINT (CAAR Q))
(PRFPRINT (CDDAR Q))
(PRINC X)
(PRINC (QUOTE / ))
(PRINC Y)
(SETQ Q (NCONC Q (LIST (CONS X (CAR Z)) (CONS Y (CDR Z)))))
P2 (SETQ Q (CDR Q))
(COND ((NULL Q) (RETURN NIL)))
(GO P1)
P3 (PRIN1 (CDR P))
(RETURN (TERPRI))))
EXPR)
(DEFPROP PROOF
(LAMBDA(L R)
(PROG (Q Q1 X Z)
(SETQ LHP L)
(SETQ RHP R)
(RPLACA (MKWRD L) 1)
(RPLACA (MKWRD R) 2)
(SETQ X 2)
(SETQ Q (LIST L R))
(SETQ Q1 Q)
P1 (SETQ Z (ANCESTOR (CAR Q)))
(COND ((ATOM (CDR Z)) (COND ((NOT (ATOM (CAR Z))) (SETQ Z (CAR Z))) (T (GO P2)))))
(RPLACA (MKWRD (CAR Z)) (SETQ X (ADD1 X)))
(RPLACA (MKWRD (CDR Z)) (SETQ X (ADD1 X)))
(NCONC Q (LIST (CAR Z) (CDR Z)))
P2 (SETQ Q (CDR Q))
(COND (Q (GO P1)))
(PRINT (QUOTE NIL))
(PRINC (CAR (MKWRD (CAR Q1))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CADR Q1))))
(SETQ X 1)
A (COND
((EQ (CAR (MKWRD (CAR Q1))) X) (PRINT X)
(PRFPRINT (CDAR Q1))
(COND
((ATOM (CAR (ANCESTOR (CAR Q1)))) (PRIN1 (CAR (ANCESTOR (CAR Q1)))))
((ATOM (CDR (ANCESTOR (CAR Q1))))
(PRINC (CAR (MKWRD (CAAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDAR (ANCESTOR (CAR Q1)))))))
(T (PRINC (CAR (MKWRD (CAR (ANCESTOR (CAR Q1))))))
(PRINC (QUOTE / ))
(PRINC (CAR (MKWRD (CDR (ANCESTOR (CAR Q1))))))))))
(SETQ Q1 (CDR Q1))
(SETQ X (ADD1 X))
(COND (Q1 (GO A)))))
EXPR)
(DEFPROP QUERY
(LAMBDA NIL
(PROG NIL
(COND (STRATEGY (PRINT (QUOTE CHOICE-STRATEGY-IS:)) (OUT >ST< (CAR (LAST STRATEGY)))))
(PRINT (QUOTE EDIT-STRATEGY-IS:))
(OUT >ST< (CAR (LAST EDITSTRAT)))
(COND ((AND (NULL PMODEL) (NULL NMODEL)) (GRINDEF MODEL))
(T (PRINT (QUOTE POSITIVE-MODEL=))
(PRINC PMODEL)
(PRINT (QUOTE NEGATIVE-MODEL=))
(PRINC NMODEL)))
(PRINT (QUOTE PARMODULATE))
(PRINC (QUOTE =))
(COND ((NOT PFLG) (PRINC T)
(PRINT (QUOTE EQUAL-SYMBOL))
(PRINC (QUOTE =))
(PRINC EQUAL)
(PRINT (QUOTE PAR-DEPTH-BOUND))
(PRINC (QUOTE =))
(PRINC PDEPTH))
(T (PRINC NIL)))
(PRINT (QUOTE ELAPSED-TIME))
(PRINC (QUOTE =))
(PRINC (TIMEIT))
(RETURN (TERPRI))))
EXPR)
(DEFPROP RESET1
(LAMBDA(L)
(PROG (X Z2 Z3 ZZ XX Z Z1 F1)
(SETQ Z STATEVECTOR)
A (COND
((EQ (CAR L) (CAR Z)) (SETQ F1 T)
(COND ((EQ (CAR L) (QUOTE STRATEGY)) (GO R1))
(T (SET (CAR Z) (EVAL (CADR L)))))))
R2 (SETQ Z1 (CONS (EVAL (CAR Z)) Z1))
(SETQ Z (CDR Z))
(COND (Z (GO A)))
(COND (F1 (RETURN (REVERSE Z1))))
R3 (PRINT (QUOTE UNDEFINED-ARG-FOR-RESET:))
(PRINC (CAR L))
(TERPRI)
(ERR NIL)
R1 (SETQ X (QUOTE (X)))
(SETQ L (CDR L))
R4 (SETQ Z2 (CAR L))
(COND ((ATOM Z2) (SETQ Z3 Z2)) (T (SETQ Z3 (CAR Z2))))
SPQ2 (COND ((NOT (MEMQ Z3 STRATLIST)) (GO R3))
((EQ Z3 (QUOTE SUPPORT)) (SETQ XX (EVAL (CADAR L)))
(PROG (ZZ)
(GO B)
A (SETQ ZZ (CONS (CDAR XX) ZZ))
(SETQ XX (CDR XX))
B (COND (XX (GO A)))
(SETQ SUPPORT ZZ))
(SETQ ZZ (QUOTE (SUPPORT C2))))
((EQ Z3 (QUOTE MODEL)) (SETQ PMODEL (CADAR L))
(SETQ NMODEL (CADDAR L))
(SETQ ZZ (CONS (CONS Z3 X) ZZ)))
((EQ Z3 (QUOTE ANCESTRY)) (SETQ ANCESTRY T))
((EQ Z3 (QUOTE ORDER)) (SETQ ORDER T))
((EQ Z3 (QUOTE MERGE)) (SETQ MERGE T))
(T (SETQ ZZ (CONS (CONS Z3 X) ZZ))))
(SETQ L (CDR L))
(COND (L (GO R4)))
(COND (ZZ (SETQ STRATEGY (QUOTE (LAMBDA (C1 C2) (SUPPORT C2))))) (T (SETQ STRATEGY NIL)))
(GO R2)))
FEXPR)
(DEFPROP SAVE1
(LAMBDA(L)
(PROG (L1 N ASLST CLST Z Z2 Z3 Z4 Z5)
(SETQ N 0)
(SETQ Z L)
A (SETQ ASLST (CONS (CONS (CAR L) N) ASLST))
(SETQ L (CDR L))
(SETQ N (ADD1 N))
(COND (L (GO A)))
(SETQ CLST (LAST Z))
(SETQ L Z)
B (SETQ Z2 (CAAR L))
(COND ((NULL (CAR Z2)) (SETQ Z3 NIL)) (T (SETQ Z3 (CAAR Z2))))
(COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
(T
(SETQ Z4
(PROG (Z Z1 N)
(SETQ N 0)
(SETQ Z1 (CDAR L))
(SETQ Z (CADR Z2))
A (COND ((EQ Z Z1) (RETURN N)))
(SETQ Z1 (CDR Z1))
(SETQ N (ADD1 N))
(GO A)))))
(SETQ Z (CDDDR Z2))
(COND ((ATOM (CDR Z))
(COND ((NOT (ATOM (CAR Z))) (SETQ Z5 (UNWIND (CAAR Z) (CDAR Z) CLST ASLST N))
(SETQ N (CDR Z5))
(SETQ Z5 (CONS NIL (CAR Z5))))
(T (SETQ Z5 (LIST Z)))))
(T (SETQ Z2 (UNWIND (CAR Z) (CDR Z) CLST ASLST N)) (SETQ Z5 (CAR Z2)) (SETQ N (CDR Z2))))
(SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
(SETQ L1 (CONS (CONS Z (CDAR L)) L1))
C (SETQ L (CDR L))
(COND (L (GO B)))
(RPLACD CLST NIL)
(RETURN (REVERSE L1))))
EXPR)
(DEFPROP SET1
(LAMBDA(L)
(PROG (TBL N)
(SETQ N 1)
(SETQ ZERO (CDAR (SETU (LIST (CONS 0 0)))))
A (SETQ TBL (CONS (CONS (CAR L) N) TBL))
(SETQ L (CDR L))
(COND (L (SETQ N (ADD1 N)) (GO A)))
(RETURN (SETU TBL))))
EXPR)
(DEFPROP SETQUERY1
(LAMBDA(X Y)
(PROG (Z)
(SETQ Z (ERRSET (SETQUERY2 X Y T)))
(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (RETURN Z)))
(RETURN (CONS (QUOTE NOPROOF) (CAR Z)))))
EXPR)
(DE UP1B(X N)(PROG NIL(TERPRI)(PRINC N)(PRINC @/ )(PRFPRINT(CDR X))))
(DEFPROP SETQUERY2
(LAMBDA(XX YY FLG)
(PROG (XYZ1 N
CHAN
Z
Z1
Z3
XYZ
Z6
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
STRATEGY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST)
(SETQ CHAN (OUTC NIL NIL))
(COND (FLG (UPDATESTATE YY)))
(SETQ XYZ1 XX)
(COND ((NULL FLG) (GO SRA1)) ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT SETQMESS)
(SETQ XX (UPDATE XX))
(SETQ XYZ1 XX)
SRA1 (COND ((NULL (CAR XX)) (SETQ XYZ1 (CDR XYZ1)) (GO SRA)))
(PRINT (QUOTE HERE-ARE-THE-CLAUSES:))
(SETQ N 1)
AA (UP1B (CAR XX) N)
(SETQ N (ADD1 N))
(SETQ XX (CDR XX))
(COND (XX (GO AA)))
SRA (COND ((AND AUTO (NULL FLG)) (SETQ Z (AUTO XYZ1)) (OUTC CHAN NIL) (RETURN Z))
(AUTO (PRINT (QUOTE (STILL-AUTO (Y / N))))
(COND
((EQ (READ) (QUOTE Y)) (SETQ Z (CONS XYZ1 (AUTO XYZ1))) (OUTC CHAN NIL) (RETURN Z)))))
SRA2 (PRINT (QUOTE DOIT-CHOICE-STRATEGY))
(SCANSET)
(START)
(SETQ Z (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z) (NULL (CAR Z))) (PRINT (QUOTE SCREWED-STRATEGY)) (GO SRA2)))
(SETQ ZIN (TOP))
(SETQ STRATEGY (LIST (QUOTE LAMBDA) (QUOTE (C1 C2)) ZIN))
(OUT >ST< ZIN)
SRB (PRINT (QUOTE DEBUG))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT DEBUG SRA SRAA) (PRINC DEBUG) (BARF NIL) (RESTRAT2 DEBUG SRA))
(T (RESTRATS DEBUG SRA)))
SRAA SRC
SRD (PRINT (QUOTE DOIT-EDIT-STRATEGY))
(SCANSET)
(START)
(SETQ Z1 (ERRSET (<ST>) T))
(SCANRESET)
(COND ((OR (NULL Z1) (NULL (CAR Z1))) (PRINT (QUOTE SCREWED-EDIT-STRATEGY)) (GO SRAA)))
(SETQ ZIN (TOP))
(SETQ EDITSTRAT (LIST (QUOTE LAMBDA) (QUOTE (C)) ZIN))
(OUT >ST< ZIN)
SRCA SRI
(PRINT (QUOTE (UNIT-REDUCTION (Y / N))))
(COND (FLG (RESTRAT UFLG SRD SRIA) (PRINC UFLG) (BARF NIL) (RESTRAT2 UFLG SRC))
(T (RESTRATS UFLG SRD)))
SRIA SRE
(PRINT (QUOTE PARAMODULATE))
(COND (FLG (PRINC (QUOTE IS))
(PRINC (QUOTE / ))
(COND (PFLG (PRINC (QUOTE N))) (T (PRINC (QUOTE Y))))
(PRINT (QUOTE (DO YOU WANT TO PARAMODULATE (Y / N))))
(SETQ Z3 (READ))
(COND ((EQ Z3 (QUOTE Y)) (SETQ PFLG NIL) (GO SRDA))
((EQ Z3 (QUOTE N)) (GO SPQ5))
((EQ Z3 ESCAPE) (PRINT (QUOTE RESETTING-TO:)) (GO SRI))
(T (GO SRE))))
(T (PRINC (QUOTE (Y / N)))
(RESTRATS Z3 SRI)
(SETQ EQUAL ESCAPE)
(COND ((EQ Z3 (QUOTE N)) (GO SPQ5)))))
SRDA (SETQ AXNO 1)
SRF (PRINT (QUOTE EQUAL-SYMBOL))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT EQUAL SRE SREA) (PRINC EQUAL) (BARF NIL) (RESTRAT2 EQUAL SRE))
(T (RESTRATS EQUAL SRE)))
SREA (SETQ PFLG NIL)
SRG (PRINT (QUOTE PAR-DEPTH-BOUND))
(PRINC (QUOTE =))
(COND (FLG (RESTRAT PDEPTH SRF SRFA) (PRINC PDEPTH) (BARF NIL) (RESTRAT2 PDEPTH SRF))
(T (RESTRATS PDEPTH SRF)))
SRFA P1
(PRINT (QUOTE DEMODULATION-LIST))
(PRINC (QUOTE =))
(PRINT (QUOTE (TYPE: 'NONE' OR 'IN' (TO INSERT))))
(COND (FLG (RESTRAT XYZ SRH SRHA) (PRINC XYZ) (BARF NIL) (RESTRAT2 XYZ SRH)) (T (RESTRATS XYZ SRG)))
SRHA (SETQ DLIST NIL)
(COND ((EQ XYZ (QUOTE NONE)) (GO SPQ6))
((EQ XYZ (QUOTE IN)) (GO P2))
(T (PRINT (QUOTE UNDEFINED-SPECIFICATION-FOR-DEMOD-LIST))))
(GO P1)
P2 (SETQ Z3 (INCLAUSES))
P2A (COND ((NULL Z3) (PRINT (QUOTE ERROR-TRY-AGAIN)) (GO P1)))
P3 (SET3 (SETQ DLIST Z3))
SRH (PRINT (QUOTE DEMOD-DEPTH-BOUND=))
(COND (FLG (RESTRAT DDEPTH P1 SRGA) (PRINC DDEPTH) (BARF NIL) (RESTRAT2 DDEPTH P1))
(T (RESTRATS DDEPTH P1)))
SRGA P6
(GO SPQ6)
SPQ5 (SETQ PFLG T)
SPQ6 (SETQ Z1
(LIST STRATEGY
SUPPORT
EDITSTRAT
MERGE
ORDER
DEBUG
DEPTH
LENGTH
ANCESTRY
PMODEL
NMODEL
PFLG
EQUAL
PDEPTH
DLIST))
(OUTC CHAN NIL)
(COND (FLG (RETURN (CONS XYZ1 Z1))) (T (RETURN Z1)))))
EXPR)
(DEFPROP SETUP
(LAMBDA(Z)
(PROG (BL Z1 Z2 Z3 Z4 Z5)
SET2 (SETQ Z3 (CAR Z))
(SETQ Z2 0)
(SETQ BL NIL)
(SETQ NO* NO)
(SETQ Z5 NIL)
S1 (SETQ Z4 (MIN1 Z3))
(COND ((NULL Z4) (GO S3)))
(UPIT Z4)
(COND ((MEMBER Z4 Z5) (GO S1)) ((POS Z4) (COND ((MEMBER (CONS ESCAPE Z4) Z5) (GO S4)))))
(SETQ Z2 (ADD1 Z2))
(SETQ Z5 (CONS Z4 Z5))
(GO S1)
S3 (SETQ Z3 NIL)
(SETQ Z4 Z5)
S2 (COND ((NEG (CAR Z4)) (SETQ Z3 Z4) (GO SET3)))
(SETQ Z4 (CDR Z4))
(COND (Z4 (GO S2)))
SET3 (SETQ Z5 (CONS (CONS Z2 (CONS Z3 (CONS 0 (CONS AXNO AXNO)))) Z5))
SET1 (SETQ Z1 (CONS Z5 Z1))
S4 (SETQ Z (CDR Z))
(COND (Z (GO SET2)))
(RETURN Z1)))
EXPR)
(DEFPROP TREE
(LAMBDA(L)
(COND ((ATOM (CDR (ANCESTOR L))) (LIST L))
(T (NCONC (LIST L) (TREE (CAR (ANCESTOR L))) (TREE (CDR (ANCESTOR L)))))))
EXPR)
(DEFPROP TREEDEP
(LAMBDA(X)
(PROG (Z)
(SETQ Z (ANCESTOR X))
(COND ((ATOM (CDR Z)) (RETURN 0)) (T (RETURN (ADD1 (MAX (TREEDEP (CAR Z)) (TREEDEP (CDR Z)))))))))
EXPR)
(DEFPROP TRY1
(LAMBDA(L)
(PROG (FILENAM PRNO POTZTBL NEWNAME TBL TIME1 Z Z2 AXNO)
(SETQ PRNO 0)
T2 (COND ((NULL L) (SETQ FILENAM (QUOTE (P R F))) (GO P3)))
(SETQ Z (CAR (LAST L)))
(SETQ FILENAM (EXPLODE (COND ((ATOM Z) Z) (T (CAR Z)))))
(EVAL (CONS (QUOTE INPUT) L))
(INC T)
P3 B (SETQ Z2 (INCLAUSES))
(INC NIL)
(COND ((NULL Z2) (RETURN NIL)))
(SETQ TIME1 (DIFFERENCE (TIME) (GCTIME)))
(SETQ Z2 (ATTEMPT Z2 NIL NIL))
A (COND ((NULL Z2) (RETURN (QUOTE *)))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL)))
((EQ (CAR Z2) (QUOTE ABORT))
(SETQ Z2 (ATTEMPT (INITIALAX1 (APPEND (CADR Z2) (CDDR Z2))) NIL NIL))))
(GO A)))
FEXPR)
(DEFPROP TRAVERSE
(LAMBDA(L)
(PROG (Z Z1 Z2)
(SETQ Z (ANCESTOR L))
(SETQ Z1 (CAR Z))
(SETQ Z (CDR Z))
(COND ((NOT (ATOM (CDR (ANCESTOR Z)))) (SETQ Z2 (TRAVERSE Z))))
(COND ((NOT (ATOM (CDR (ANCESTOR Z1)))) (SETQ Z2 (NCONC (TRAVERSE Z1) Z2))))
(RETURN (COND ((HERE L) (CONS L Z2)) (T Z2)))))
EXPR)
(DEFPROP UPDATE
(LAMBDA(E)
(PROG (USINGFL USING
CHAN1
ELOC
CHAN
AUTO
DL1
RF
XYZ
XYZ1
CMD
LOCFLG
Z
Z1
Z2
INCT
Z3
UEX
Z1R
Z2R
N1
R
N
NAME
NAMELIST
ZZ)
(SETQ CHAN (OUTC NIL NIL))
(SETQ AXNO (QUOTE INSERT))
(SETQ FNNAM (QUOTE EDI))
(SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
(SETQ N1 (LAST NAMELIST))
(SETQ INCT (INC NIL))
U9 (SETQ ELOC E)
(SETQ N 1)
U3 (UP1A (CAR ELOC) N)
U3A (TERPRI)
U3AA (SETQ CMD (READ))
(COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
U3B (COND ((NOT (ATOM CMD)) (GO UPDATE1)))
U3C (SETQ CMD (EXPLODE CMD))
(COND ((EQ (LENGTH CMD) 1) (GO UER1))
((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
(GO U3A)
UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
(GO U3A)
UDI1 (SETQ Z1 (UPGETL E NAMELIST))
(COND ((NULL Z1) (GO U3A)))
(CLAUSES Z1)
(GO U3A)
USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
(SETQ Z NAMELIST)
USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
(SETQ Z (CDR Z))
(COND (Z (GO USY2)))
(GO U3A)
UFL2 (SETQ Z (QUOTE U))
(GO UFL4)
UFL3 (SETQ Z (QUOTE D))
(GO UFL4)
UFL1 (SETQ Z (CAR (EXPLODE (READ))))
UFL4 (SETQ Z2 405104)
(COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
(COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
(UPDATESTATE (CDDR Z))
(GO U3A)
UDE1 (SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
(EXPUNGE Z2)
(GO U3A)
UIN1 (SETQ NAME (READ))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (GO U3A)))
(COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
(NCONC Z1 Z2)
(GO U3A)
USU1 (SETQ Z1 (ERRSET (GETTERMS)))
(COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
((NULL (CAR Z1)) (GO U3A)))
(SETQ Z3 NIL)
(SETQ Z1 (CAR Z1))
USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (GO U12B)))
UUP1 (SETQ Z2 (UPGETNU))
(COND ((NUMBERP Z2) (GO U8)) (T (GO U3A)))
UDO1 (SETQ Z2 (UPGETNU))
(COND ((NUMBERP Z2) (GO U7)) (T (GO U3A)))
UAN1 (SETQ Z2 (UPGETL E NAMELIST))
UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
(SETQ Z2 (CDR Z2))
(GO UAN2)
UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
(INC INCT)
(OUTC CHAN NIL)
(SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
(SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
(RETURN (MINIMIZE (APPEND Z1 Z)))
USA1 (SETQ Z2 (UPGETL E NAMELIST))
(COND (Z2 (NCONC E Z2)))
(GO U3A)
UPA1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
(COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
(COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
(SETQ Z3 Z1)
USI2 (DEMOD (LIST (CAR Z3)) Z2)
(SETQ Z3 (CDR Z3))
(COND (Z3 (GO USI2)))
(PRINT (QUOTE CLAUSES-ARE:))
(CLAUSES Z1)
(GO U3A)
UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
(GO UUS3)
UCU1 (QUERY)
(GO U3A)
UDS1 (SETQ Z1 (READ))
(COND ((NOT (ATOM Z1)) (GO UDS3)))
UDS2 (COND
((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
(GO UDS2)))
UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
(GO U3A)
UEO1 (OUTC CHAN1 T)
(GO U3A)
UUS1 (SETQ NAME (QUOTE %USING))
(SETQ USINGFL T)
(SETQ USING NIL)
UUS3 (SETQ LOCFLG T)
UUS2 (SETQ Z2 (UPGETL E NAMELIST))
(SETQ USINGFL NIL)
(COND ((NULL Z2) (GO U3A)))
USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
(COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
(T (RPLACA (CAR N1) NAME)
(RPLACD (CAR N1) Z2)
(RPLACD N1 (CONS (CONS NIL NIL) NIL))
(SETQ N1 (CDR N1))))
(GO U3A)
USE1 (SETQ NAME (READ))
(SETQ LOCFLG NIL)
(GO UUS2)
UCL1 (SETQ Z (READ))
UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
(GO UCL2))
(T (GO U3A)))
UGO1 (SETQ Z1 (UPGETNU))
(COND ((NOT (NUMBERP Z1)) (GO U3A)))
(COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
(T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
UTR1 (SETQ UEX NIL)
(GO UEX2)
UEX1 (SETQ UEX T)
UEX2 (SETQ NAME (QUOTE LEMMA))
(SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
(COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
(SETQ AUTO T)
(SETQ Z2
(ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
(COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
(T NIL))
NIL))
(SETQ AUTO NIL)
(GO AT1A)
UST1 (STOP)
(GO U3A)
UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
(ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
U8 (COND ((EQ Z2 0) (GO U9)))
U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
(SETQ Z2 (DIFFERENCE Z2 5))
(SETQ ZZ 5)
U84 (SETQ Z N)
(SETQ Z3 (DIFFERENCE N ZZ))
(COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
(SETQ N Z3)
(SETQ Z3 ELOC)
(SETQ ELOC (DOWN N E))
(SETQ ZZ NIL)
(SETQ Z1 ELOC)
U81 (COND ((EQ Z1 Z3) (GO U82)))
(SETQ ZZ (CONS (CAR Z1) ZZ))
(SETQ Z1 (CDR Z1))
(GO U81)
U82 (COND ((NULL ZZ) (GO U83)))
(UP1A (CAR ZZ) (SUB1 Z))
(SETQ ZZ (CDR ZZ))
(SETQ Z (SUB1 Z))
(GO U82)
U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
(SETQ Z2 (PLUS Z2 N))
U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
(SETQ ELOC (CDR ELOC))
(SETQ N (ADD1 N))
(UP1A (CAR ELOC) N)
(COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
UPR1 (TERPRI)
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
(COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
(SETQ AXNO (QUOTE THEOREM))
(SETQ Z3 (NEGATE (CAR Z2)))
(SETQ AXNO (QUOTE INSERT))
(SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
(COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
(SETQ NAME (QUOTE LEMMA))
(SETQ LOCFLG T)
(GO USE2)
UME1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(BAKSUB Z1 Z2)
(GO U3A)
UHE1 (PRINT MESSAGE)
(GO U3A)
URE1 (SETQ Z1 (UPGETL E NAMELIST))
(SETQ Z2 (UPGETL E NAMELIST))
U%RE1
(SETQ RF T)
URE1A
(COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
(SETQ Z1R Z1)
(SETQ Z2R Z2)
(SETQ Z3 NIL)
(COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
(COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
(COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
(COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
(SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
UR3A (SETQ Z2R (CDR Z2R))
(COND (Z2R (GO UR3)))
(SETQ Z1R (CDR Z1R))
(COND (Z1R (SETQ Z2R Z2) (GO UR3)))
UR3B (COND ((NULL Z3)
(COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
(T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
(RF (SETQ NAME (QUOTE RES)))
(T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
(SETQ Z2 Z3)
(SETQ LOCFLG T)
(GO AT2A)
UEV1 (PRINT (QUOTE EVAL-AWAITS))
(SETQ Z2 (ERRSET (EVAL (READ)) T))
(COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
(GO UEV1)
UPDATE1
(SETQ Z (EXPLODE (CAR CMD)))
(COND ((SETQ Z (ASSOC (READLIST (LIST (CAR Z) (CADR Z))) GOLIST1)) (GO (CDR Z))) (T (GO UER1)))
AT1 (COND ((NULL (SETQ Z1 (GETNAME (CADR CMD) NAMELIST))) (GO U3A)))
(SETQ NAME (CADR CMD))
(SETQ XYZ Z1)
(RPLACA (CDR CMD) (QUOTE XYZ))
(RPLACA CMD (QUOTE ATTEMPTUNTIL))
(SETQ Z2 (EVAL CMD))
AT1A (UPDATESTATE STRAT)
(COND
((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
(PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
(PRINC NAME)
(GO U3A))
((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
(SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
(SETQ AUTO NIL)
(GO AT1A))
((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
(SETQ Z2 (CADR Z2))
AT2A (SETQ N 1)
AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
(SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
(PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
(PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
(PRIN1 NAME)
(CLAUSES Z2)
(GO USE2)
S1 (COND ((NULL (SETQ XYZ (GETNAME (CADDDR CMD) NAMELIST))) (GO U3A)))
(RPLACA (CDDDR CMD) (QUOTE XYZ))
(RPLACA CMD (QUOTE SAVE))
(EVAL CMD)
(GO U3A)))
EXPR)
(DEFPROP UPGETL
(LAMBDA(E N)
(PROG (C N1 Z Z1 Z2 Z3 ZZ N2)
(SCANSET)
(START)
(SETQ C (ERRSET (<CLAUSES>) T))
(SCANRESET)
(COND ((OR (NULL C) (NULL (CAR C))) (PRINT (QUOTE LOSSAGE-IN-CLAUSES)) (RETURN NIL)))
(SETQ C (TOP))
(COND ((EQ C (QUOTE EMPTY)) (RETURN NIL)))
AS1 (SETQ Z (CAR C))
(COND ((ATOM Z)
(COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
(COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
(T (RETURN NIL))))
((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
(T (RETURN NIL))))
((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
(T (RETURN NIL)))
AS6 (SETQ C (CDR C))
(COND (C (GO AS1)) (T (RETURN ZZ)))
AS2 (SETQ Z2 (CADR Z))
(SETQ N1 (CAR Z))
(SETQ Z (CDR Z))
(SETQ Z3 Z1)
AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
AS3 (SETQ Z2 (SUB1 Z2))
(COND ((ZEROP Z2) (GO AS4)))
(SETQ Z1 (CDR Z1))
(COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
AS4 (COND
((NOT (HERE (CAR Z1))) (PRINT N1)
(PRINC (QUOTE / ))
(PRINC (CAR Z))
(PRINC (QUOTE / ))
(PRINC (QUOTE HAS-BEEN-DELETED))
(RETURN NIL)))
(SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
(SETQ Z (CDR Z))
(COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
(GO AS6)
AS10 (SETQ N2 (QUOTE INSERT))
(SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF (FIXQFF (CDR Z)))))))
(GO AS6)
AS20 (SETQ N2 (QUOTE MATCHES))
(SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
(COND ((NULL Z) (GO AS6)) (T (GO AS31)))
AS30 (SETQ N2 (QUOTE INPUT))
(SETQ ZIN (CDR Z))
(COND
((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
(INC T)
(SETQ Z (INCLAUSES))
(INC NIL)
(COND ((NULL Z) (RETURN NIL)))
AS31 (SETQ ZZ (APPENDIT ZZ Z))
(GO AS6)))
EXPR)